A:Type, eq:EqDecider(A), B:Top, x, y:A, v, u:Top. x = y  x : v || y : u 

latex

Definitions	False, P  Q, A, t  T, Top, x.A(x), x:A. B(x), x. t(x), x : v, x  dom(f), b, x:AB(x), Prop, P & Q, x:AB(x), f(a), x(s), s = t, f || g, Type, EqDecider(T), left+right, P  Q, Void, <a,b>, eqof(d), P  Q, P  Q, false, p  q
Lemmas	assert of bor, bor wf, bfalse wf, and functionality wrt iff, or functionality wrt iff, deq property, eqof wf, false wf, not wf, deq wf, assert wf, fpf-dom wf, fpf-single wf, top wf